Nuprl Lemma : ratio-dist_wf
0,22
postcript
pdf
a
,
p
:
,
b
,
q
:
,
m
:
. |
a
/
b
-
p
/
q
| < 1/
m
Prop
latex
Definitions
,
t
T
,
,
{
x
:
A
|
B
(
x
) }
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
n
m
,
n
-
m
,
|
i
|
,
a
<
b
,
Type
,
Prop
,
|
a
/
b
-
p
/
q
| < 1/
m
Lemmas
absval
wf
,
nat
plus
wf
,
nat
wf
origin
a, p:
, b, q:
, m:. |a/b - p/q| < 1/m 
Prop a, p:, b, q:, m:. |a/b - p/q| < 1/m Prop T
B(x)x:A. B(x)
m